x:Id, k:Knd, ds:x:Id fp Type, da:a:Knd fp Type, f:Top, x1:Id, k1:Knd, d1:x:Id fp Type,
d2:a:Knd fp Type, f1:Top.
ds || d1
 da || d2
 <k,x> = <k1,x1>
 (with declarations 
 (ds:ds
 (da:da
 (effect of k(v) is x := f s v
 (||+ with declarations 
 (||+ ds:d1
 (||+ da:d2
 (||+ effect of k1(v) is x1 := f1 s v) 

latex

Definitions

False, P  Q, A, t  T, x:AB(x), x:A. B(x), Id, <a,b>, Type, IdDeq, f  g, State(ds), Knd, KindDeq, Valtype(da;k), 2of(t), Void, f(x)?z, s = t, x:AB(x), f(a), 1of(t), type List, (x  l), deq-member(eq;x;L), b, Prop, P & Q, x.A(x), P  Q, P  Q, {T}, x. t(x), EqDecider(T), product-deq(A;B;a;b), left+right, P  Q, false, eqof(d), f(x), x  dom(f), f || g, AB, , {x:A| B(x) }, , a:A fp B(a), x:A. B(x), Top, Case b of inl(x)  s(x) ; inr(y)  t(y), if b t else f fi, #$n, a<b, Atom, nil, M.state, M.da(a), (s1  s2 mod x), M.dout(l,tg), xL. P(x), IdLnk, p  q, , xdom(f). v=f(x)   P(x;v), z != f(x)  P(a;z), M.rframe(A.sends tfL of k on l), M.sframe(k sends <l,tg>), M.rframe(A.effect f of k on y), M.aframe(k affects x), M.frame(k affects x), M.rframe(A.pre p for a), ma-frame-compat(A;B), ma-frame-compatible(A;B), mk-ma, , x : v, with declarations ds:dsda:daeffect of k(v) is x := f s v, A & B, rcv(l,tg), locl(a), M1 ||decl M2, M1 || M2, A ||+ B

Lemmas

not wf, fpf-compatible wf, top wf, fpf wf, bor wf, IdLnk wf, or functionality wrt iff, false wf, assert of bor, eqof wf, bfalse wf, deq property, product-deq wf, Kind-deq wf, Knd wf, all functionality wrt iff, implies functionality wrt iff, and functionality wrt iff, assert-deq-member, assert wf, deq-member wf, l member wf, id-deq wf, Id wf, locl one one